w:World, e:E, i:Id. (i = loc(e))  ((isnull(a(i;time(e))))) 

latex

Definitions	t  T, {T}, P  Q, x:A. B(x), SQType(T), Id, s = t, , s ~ t, Atom$n, , Type, x.A(x), x. t(x), t.1, t.2, a(i;t), isnull(a), b, Void, x:AB(x), False, A, {x:A| B(x)} , E, World, time(e), loc(e)
Lemmas	w-E wf, world wf, assert wf, w-isnull wf, w-a wf, pi2 wf, pi1 wf, nat wf, Id wf, Id sq